\begin{tabbing}
strong\_before($x$; $y$; $l$; $T$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($x$ $\in$ $l$ $\in$ $T$) \& ($y$ $\in$ $l$ $\in$ $T$)\+
\\[0ex]\& ($\forall$$i$:$\mathbb{N}$, $j$:$\mathbb{N}$. $i$$<\parallel$$l$$\parallel$ $\Rightarrow$ $j$$<\parallel$$l$$\parallel$ $\Rightarrow$ $l$[$i$] $=$ $x$ $\in$ $T$ $\Rightarrow$ $l$[$j$] $=$ $y$ $\in$ $T$ $\Rightarrow$ $i$$<$$j$)
\-
\end{tabbing}